Search for: All records

While machine learning has been adopted across various fields, its ability to outperform traditional heuristics in operating systems is often met with justified skepticism. Concerns about unsafe decisions, opaque debugging processes, and the challenges of integrating ML into the kernel—given its stringent latency constraints and inherent complexity — make practitioners understandably cautious. This paper introduces Guardrails for the OS, a framework that allows kernel developers to declaratively specify system-level properties and define corrective actions to address property violations. The framework facilitates the compilation of these guardrails into monitors capable of running within the kernel. In this work, we establish the foundation for Guardrails, detailing its core abstractions, examining the problem space, and exploring potential solutions. 

P4Cub is a new intermediate representation (IR) for the P4 programming language. It has been designed with the goal of facilitating development of certified tools. To achieve this, P4Cub is organized around a small set of core constructs and avoids side effects in expressions, which avoids mutual recursion between the semantics of expressions and statements. Still, it retains the essential domain-specific features of P4 itself. P4Cub has a front-end based on Petr4, and has been fully mechanized in Coq including big-step and small-step semantics and a type system. As case studies, we have engineered several certified tools with P4Cub including proofs of type soundness, a verified compilation pass, and an automated verification tool. 

Introducing charge carriers is of paramount importance for increasing the efficiency of organic semiconducting materials. Various methods of extrinsic doping, where molecules or atoms with large/small reduction potentials are blended with the semiconductor, can lead to dopant aggregation, migration, phase segregation, and morphology alteration. Self-doping overcomes these challenges by structurally linking the dopant directly to the organic semiconductor. However, for their practical incorporation into devices, self-doped organic materials must be cast into thin-films, yet processing methods to allow for the formation of continuous and uniform films have not been developed beyond simple drop-casting. Whilst self-doped organic molecules afford the remarkable ability to position dopants with molecular precision and control of attachment mode, their steric bulk inevitably disrupts the crystallization on surfaces. As such, there is great interest in the development of processing modalities that allow deposited molecules to converge to the thermodynamic minimum of a well-ordered and highly crystalline organic thin film instead of getting trapped in local disordered minima that represent metastable configurations. By contrasting drop casting, ultrasonic deposition, and physical vapor deposition, we investigate the free energy landscape of the crystallization of sterically hindered self-doped perylene diimide thin films. A clear relationship is established between processing conditions, the crystallinity and order within the deposited films, the dopant structures and the resulting spin density. We find physical vapor deposition to be a robust method capable of producing smooth, continuous, highly ordered self-doped organic small molecule thin-films with tailored spin concentrations and well-defined morphologies.